$\forall$$k$:$\mathbb{N}$, $f$:(int\_seg(0; $k$)$\rightarrow\mathbb{Z}$).
\\[0ex]increasing($f$; $k$) $\Rightarrow$ guard(($\forall$$x$,$y$:int\_seg(0; $k$). ($x$ $<$ $y$) $\Rightarrow$ (($f$($x$)) $<$ ($f$($y$)))))